Nuprl Lemma : comp_assoc
12,41
postcript
pdf
A
,
B
,
C
,
D
:Type,
f
:(
A
B
),
g
:(
B
C
),
h
:(
C
D
). (
h
o (
g
o
f
)) = ((
h
o
g
) o
f
)
A
D
latex
ProofTree
Definitions
t
T
,
f
o
g
,
x
:
A
.
B
(
x
)
origin
A, B, C, D:Type, f:(A
B), g:(BC), h:(CD). (h o (g o f)) = ((h o g) o f) 
AD
A, B, C, D:Type, f:(AB), g:(BC), h:(CD). (h o (g o f)) = ((h o g) o f) AD
Tx:A. B(x)